\documentclass[12pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[brazilian]{babel}
\usepackage{graphicx}
\usepackage{caption}
\usepackage{hyphenat}
\usepackage{listings}
\usepackage{dinossauro}

\hyphenation{re-gis-tra-dor}

\begin{document}

\include{capa}

\tableofcontents

\newpage

\section{Introdução}

Uma das aplicações mais comuns de técnicas de verificação automática (\textit{model checking}) é na área de desenvolvimento de \textit{hardware}, em que essas técnicas são aplicadas para validação das propriedades dos circuitos projetados.

Nesse sentido, o presente trabalho realiza a implementação de um processador $\mu$RISC adaptado, com o objetivo de verificar a validade de propriedades importantes de cada um dos módulos que o compõem.

O processador $\mu$RISC, como o nome sugere, é a implementação de uma forma simplificada do conjunto de instruções RISC, apresentando barramentos de 16 bits, contra 32 bits dos barramentos de um RISC comum. %em que os endereços são alinhados na memória, diferentemente da arquitetura \textit{CISC}.

Este trabalho foi implementado com o auxílio da ferramenta de \textit{model checking} simbólico NuSMV versão 2.5.0, que mistura verificação baseada em BDDs com verificação baseada em SAT. Foi desenvolvido em ambiente Linux com utilização de especificações em LTL para modelagem das propriedades a serem verificadas.

A listagem completa do código deste trabalho pode ser encontrada no apêndice deste documento.

\section{Arquitetura}

\subsection{Decisões de Implementação}

O processador original executa instruções em um único ciclo, mas para este trabalho o processador foi elaborado para executar instruções em multi-ciclo. Isso permite que várias instruções estejam no pipeline ao mesmo tempo, embora a unidade de controle para realizar o \textit{forwarding} de dados no caso de instruções com dependências não tenha sido implementada, por motivos de simplificação.

Quanto ao tamanho da palavra desse processador, optou-se por fazê-la de 8 bits, uma vez que tentativas de implementar o processador com palavras de 16, 12 e 10 bits mostraram-se inviáveis, pois em nenhum desses casos conseguiu-se provar (ou obter um contra-exemplo) em tempo razoável nenhuma das propriedades a serem verificadas. Para palavras de 12 bits, por exemplo, em mais de 40 minutos nenhuma das propriedades havia sido provada nem um contra-exemplo havia sido encontrado. Essa decisão limita bastante a quantidade de operações que podem ser realizadas por esse processador ou o número de bits para endereçar registradores, uma vez que tem-se um número menor de bits para os respectivos campos da instrução. 

Na implementação feita, optou-se por privilegiar a variedade de instruções em vez do número de registradores endereçáveis, dando um número maior de bits para o identificador da instrução (opcode) do que para os campos que endereçam os registradores envolvidos na operação.

%\newpage

\subsubsection{Datapath}

A Figura 1 ilustra a organização de um processador multiciclo, como o que será verificado neste trabalho.

\begin{figure}[h]
\begin{center}
	\includegraphics[scale=0.50]{multi_cycle_cpu_datapath.png}
	\label{datapath}
        \caption{Caminho de Dados de Referência}
\end{center}
\end{figure}

\subsubsection{Formato das Instruções}

O processador implementado possui instruções de apenas 2 registradores, de forma a facilitar a representação dos operadores de uma instrução no espaço de 8 bits da palavra. Dessa forma, uma instrução do tipo \texttt{ADD R1,R2} define a soma entre os registradores \texttt{R1} e \texttt{R2} e o armazenamento do resultado no primeiro registrador (\texttt{R1}).

A palavra do processador é, então, dividida em três partes, como ilustrado no exemplo abaixo.

\begin{center}
\texttt{01 10 0001}
\end{center}

A primeira parte, correspondente aos 2 bits mais à esquerda, é reservada para identificação do primeiro registrador envolvido na operação. O segundo grupo de 2 bits corresponde, similarmente, à identificação do segundo registrador envolvido na operação. Por fim, os quatro bits mais à direita identificam a instrução sendo executada (opcode). Essa divisão da palavra do processador foi feita privilegiando-se a variedade de instruções disponíveis, em detrimento do número de registradores gerais possíveis de se endereçar.

\subsubsection{Conjunto de Instruções}

São doze as instruções implementadas: oito operações de ALU; duas operações de memória; e uma de desvio incondicional. Todas elas estão discriminadas na Tabela \ref{instrucoes} com seus respectivos opcodes e representações.

\begin{table}[h]
  \begin{center}
    \begin{tabular}{|c|c|c|}
      \hline
      \textbf{Opcode} & \textbf{Instrução} & \textbf{Representação} \\ \hline
      0000 & Soma & a = a + b \\ \hline
      0001 & Subtração & a = a - b \\ \hline
      0010 & Multiplicação & a = a * b \\ \hline
      0011 & Divisão & a = a / b \\ \hline
      0100 & And & a = a \& b \\ \hline
      0101 & Or & $a = a | b$ \\ \hline
      0110 & Not & a = !a \\ \hline
      0111 & Xor & a = a xor b \\ \hline
      1000 & Xnor & a = a xnor b \\ \hline
      1001 & Jump & end = instrução[7:4] \\ \hline
      1010 & Load & Carrega da memóra \\ \hline
      1011 & Write & Escreve na memória \\ \hline
    \end{tabular}
    \caption{Conjunto de Instruções}
    \label{instrucoes}
  \end{center}
\end{table}


\subsection{Descrição dos módulos}

A descrição de todos os módulos do processador é dada na sequência. Vale ressaltar que toda operação de leitura é realizada assincronamente, enquanto toda operação de escrita é feita de forma síncrona, na borda positiva do \textit{clock}. \\

\textbf{Cache de Instruções} \\

Esse módulo implementa uma memória de 8 posições de palavras de 8 bits, cuja finalidade é armazenar as próximas instruções a serem executadas. Recebe dois parâmetros como entrada, como mostrado abaixo. \\

\texttt{MODULE cache\_i(address, rd)} \\

O primeiro parâmetro corresponde ao endereço da cache a ser lido para obtenção da próxima instrução, enquanto o segundo parâmetro corresponde ao pino de leitura. O valor desse pino define se a instrução na posição \texttt{address} da cache será lida para a porta de saída. \\

\textbf{Cache de Dados} \\

A cache de dados implementa uma memória de 8 posições de 3 bits cada, com a finalidade de armazenar dados. Recebe 5 parâmetros na entrada, como mostrado no cabeçalho abaixo. \\

\texttt{MODULE cache\_d(address, data, clock, rd, wr)} \\

O primeiro parâmetro corresponde ao endereço da cache de onde o dado será lido ou escrito. O parâmetro \texttt{data} corresponde ao dado a ser escrito, quando uma escrita na cache for realizada. O parâmetro \textit{clock} é utilizado para a sincronização da operação de escrita na cache. Os dois últimos parâmetros são os pinos de leitura e escrita, respectivamente, que definem quando uma leitura ou escrita na cache deve ser realizada. \\

\textbf{Instruction Fetch} \\

O módulo de busca por instruções recebe como parâmetros o valor do \textit{clock} e a próxima instrução a ser executada, obtida da Cache de Instruções, como mostrado no cabeçalho desse módulo. \\

\texttt{MODULE fetch(clock, instrucao)} \\

É responsável simplesmente por passar a instrução a ser executada para frente no pipeline, na próxima borda positiva do \textit{clock}. \\

\textbf{Módulo Banco de Registradores} \\

Este módulo recebe seis parâmetros de entrada, como mostrado em seu cabeçalho. \\

\texttt{MODULE banco\_reg(addr1, addr2, addr\_w, dado\_w, clock, wr)} \\

Os dois primeiros parâmetros são os endereços dos registradores cujos valores devem ser lidos. O terceiro é o endereço de escrita, usado quando é necessário gravar um valor em algum registrador do banco. O quarto parâmetro é o valor que será gravado no registrador, caso esteja sendo realizada uma escrita. O penúltimo parâmetro é o \textit{clock}, que serve para sincronizar as atividades dos módulos. Por fim, o último parâmetro é o valor do pino de escrita, que define se será realizada uma escrita em um registrador do banco de dados.

As funções deste módulo são as de colocar em suas portas de saída os valores dos registradores que devem ser lidos e, caso o pino de escrita esteja ativado, gravar o valor passado no registrador identificado pelo parâmetro \texttt{addr\_w}. \\

\textbf{Módulo Decode} \\

O módulo de decodificação recebe dois parâmetros na entrada, como mostrado no cabeçalho abaixo. \\

\texttt{MODULE decode(clock, data\_in)} \\

O primeiro parâmetro é o \textit{clock} e o segundo corresponde à instrução a ser decodificada.

A responsabilidade deste módulo é de decodificar a instrução, obtendo os valores dos campos referentes aos dois registradores e o opcode da instrução. \\

\textbf{Módulo Execute e ALU} \\

A ALU é o módulo de fato responsável pela execução da instrução, recebendo como parâmetros os dois valores envolvidos na operação e o opcode da instrução. De acordo com o valor de opcode, a ALU executa a operação (adição, por exemplo) com os dois valores e coloca na porta de saída o resultado do cálculo. O cabeçalho desse módulo é mostrado a seguir. \\

\texttt{MODULE alu(a,op,b)} \\

O módulo de execução serve apenas para efeito de sincronização, passando à frente no pipeline o opcode da instrução executada e o endereço de escrita do dado calculado pela ALU. Seus parâmetros são mostrados abaixo. \\

\texttt{MODULE execute(clock, opcode, addr\_w, data\_w)} \\

\textbf{Módulo de extensão de sinal} \\

Módulo responsável por estender um valor dado em 12 bits para o correspondente em 16. Recebe um único parâmetro, o valor a ser estendido, como mostrado em seu cabeçalho. \\

\texttt{MODULE ext\_signal(num)} \\

\textbf{Módulo Mem} \\

Esse módulo tem a função de passar à frente no pipeline o opcode da instrução, o endereço da memória sobre o qual será feita a operação e o valor que será escrito, no caso de uma escrita. Essas informações provém da própria instrução que, no caso de uma operação em memória, armazena em seu primeiro campo (3 bits mais à esquerda) o endereço da memória e, em seu segundo campo (os 3 bits seguintes), o valor a ser salvo.

Os parâmetros desse módulo são mostrados abaixo. \\

\texttt{MODULE mem(clock, reg1, reg2, opcode)} \\

\textbf{Módulo WriteBack} \\

Esse módulo é simplesmente responsável por ativar o pino de escrita da memória, de acordo com o opcode da instrução, e passar à frente no pipeline o endereço e o valor de escrita. Os parâmetros desse módulo são mostrados abaixo. \\

\texttt{MODULE write\_back(clock, opcode, addr\_w, data\_w)}


\section{Resultados}

Nas subseções seguintes são apresentadas as propriedades verificadas em cada um dos módulos do processador implementado, com comentários sobre as mais relevantes. Vale ressaltar que para algumas delas não foi possível obter o resultado dado pelo NuSMV devido ao tempo de execução demasiadamente elevado, então optou-se por provar essas propriedades por partes, executando um subconjunto delas de cada vez.

Como os módulos do processador são independentes entre si, as propriedades foram sendo provadas assim que cada módulo ia sendo implementado, obtendo-se ao final a verificação do processador como um todo. Isso viabilizou uma implementação mais segura, visto que o funcionamento correto dos módulos era garantido pelas suas respectivas propriedades provadas.

Para mais detalhes sobre o significado das variáveis utilizadas nas propriedades, vide a listagem completa do código no apêndice deste documento.

\subsection{Propriedades do Módulo Main}

As principais propriedades desse módulo verificam se os valores passados de um estágio do pipeline para outro são coerentes.

\begin{codigoMargem}
SPEC AF ( clock = 1)

LTLSPEC F ( cacheInst.output = 0d8_0 )
  
LTLSPEC F ( pc = 0d4_0 )

-- Verifica se a instrucao obtida da cache
-- de instrucoes e' a mesma quem no proximo
-- estado, chega ao modulo de Fetch
LTLSPEC X ( cacheInst.output = 0d8_2 -> 
	    X if_mod.data_out = 0d8_2 )

-- Verifica se o primeiro registrador da
-- instrucao recebida e passado corretamente
-- para o modulo de decode no proximo estado
LTLSPEC X ( if_mod.data_out[7:6]= 0d2_2 -> 
	    X dec_mod.reg1 = 0d2_2 )

-- Verifica se a instrucao e passada da cache
-- de instrucoes para o modulo de Fetch no
-- posedge do clock
LTLSPEC F ( clock = 1 -> 
	    X cacheInst.output = if_mod.data_out )
\end{codigoMargem}


\subsection{Propriedades do Módulo ALU}

Essas propriedades verificam o funcionamento das principais funções implementadas pela ALU. Todas elas visam verificar se, em qualquer estado, as respectivas operações produzem o resultado esperado para os valores dados.

\begin{codigoMargem}
-- Propriedade para o +
LTLSPEC G ( op = 0b4_0001 & a = 0d16_10 & b = 0d16_10 ->
            output = 0d16_20 )
-- Propriedade para o -
LTLSPEC G ( op = 0b4_0001 & a = 0d16_10 & b = 0d16_6 ->
            output = 0d16_4 )

-- Propriedade para o *
LTLSPEC G ( op = 0b4_0001 & a = 0d16_10 & b = 0d16_3 ->
            output = 0d16_30 )
-- Propriedade para o /
LTLSPEC G ( op = 0b4_0100 & a = 0d16_10 & b = 0d16_2 -> 
            output = 0d16_5 )

-- Propriedade para o not
LTLSPEC G ( op = 0b4_0111 & a = 0b16_00001010 ->
            output = 0b16_11110101 )

-- Propriedade para o and
LTLSPEC G ( op = 0b4_0101 & a = 0b16_00001010 
            & b = 0b16_11111111
            -> output = 0b16_00001010 )

-- Propriedade para o or
LTLSPEC G ( op = 0b4_0110 & a = 0b16_01001010 
            & b = 0b16_00011001 
            -> output = 0b16_01011011 )

-- Propriedade para o xor
LTLSPEC G ( op = 0b4_0110 & a = 0b16_1010 & b = 0b16_1001 
            -> output = 0b16_0011 )

-- Propriedade para o xnor
LTLSPEC G ( op = 0b4_0110 & a = 0b16_1010 & b = 0b16_1001 
            -> output = 0b16_1100 )
\end{codigoMargem}

\subsection{Propriedades do Módulo Cache de Instruções}

As propriedades básicas a serem verificadas nesse módulo é se a cache de instruções é sempre lida (lida em todo ciclo do processador) e se o conteúdo do barramento de saída da cache é o mesmo contido no endereço solicitado.

\begin{codigoMargem}
-- Sempre eh feito leitura da cache de instrucoes
SPEC AG ( rd = 1)  

-- Verificando se o barramento de saida esta coerente 
-- com a memoria
LTLSPEC G ( output = mem[address] )

LTLSPEC G ( mem[5] = 0d8_5 )
\end{codigoMargem}

\subsection{Propriedades do Módulo Cache de Dados}

Nesse módulo, fazem-se verificações de coerência nos momentos de leitura e escrita na cache. No caso da escrita, no próximo estado o endereço da cache a receber o valor deve conter exatamente o valor passado, quando o clock estiver em sua borda positiva. No caso da leitura, o dado no barramento de saída deve ser o mesmo encontrado no endereço da cache que foi consultado.

\begin{codigoMargem}
-- Verificando a escrita em memoria
LTLSPEC G ( wr & clock -> X mem[address] = data )

-- Verificando a leitura da memoria
LTLSPEC G ( rd -> mem[address] = output )
\end{codigoMargem}


\subsection{Propriedades do Módulo Banco de Registradores}

Também nesse módulo são feitos testes de coerência na escrita e na leitura.

\begin{codigoMargem}
-- Verificando a consistencia de escrita no banco de
-- registradores
LTLSPEC X ( addr_w = 0d2_0 & dado_w = 0d16_5
            -> banco[0] = 0d16_5 )

-- Verificando a consistencia de leitura no banco 
-- de registradores
LTLSPEC G ( banco[addr1] = output1 )

LTLSPEC G ( output1 = output2 )
\end{codigoMargem}


\subsection{Propriedades do Módulo Fetch}

Aqui verifica-se simplesmente se o endereço de busca da instrução está dentro dos limites corretos.

\begin{codigoMargem}
LTLSPEC G ( address >= 0d2_0 & address <= 0d2_3 )
\end{codigoMargem}

\subsection{Propriedades do Módulo Decode}

A propriedade deste módulo simplesmente verifica se os valores dos campos da instrução foram lidos corretamente.

\begin{codigoMargem}
LTLSPEC G ( data_in[7:6] = reg1 & data_in[5:4] = reg2 
            & data_in[3:0] = opcode )
\end{codigoMargem}

\subsection{Propriedades do Módulo Execute}

Como a única função deste módulo é de sincronia (passando os dados para frente no pipeline), a única propriedade a ser verificada é a de coerência do que é recebido por este módulo e do que ele passa para o estágio seguinte.

\begin{codigoMargem}
LTLSPEC G ( opcode_out = opcode & addr_out = addr_w
	    & data_out = data_w )
\end{codigoMargem}

\subsection{Propriedades do Módulo Memória}

A verificação feita nesse módulo é novamente de coerência na passagem de dados para o próximo estágio do pipeline.

\begin{codigoMargem}
LTLSPEC G ( clock & reg2 = 0d16_5 -> X data_out = 0d16_5 )
\end{codigoMargem}

\subsection{Propriedades do Módulo Write Back}

A propriedade mais importante a ser verificada nesse estágio do pipeline é se a escrita de volta no banco de registradores está sendo feita corretamente. Vide o código completo listado no apêndice deste documento para mais detalhes.

\begin{codigoMargem}
-- Verificando se a escrita de volta nos registradores 
-- eh feita no posedge do clock
LTLSPEC G (opcode = 0d4_0 & clock <-> write)
\end{codigoMargem}

\subsection{Propriedades do Módulo Extensão de Sinal}

Basicamente verifica se as extensões de sinais estão sendo feitas corretamente (acrescentando 0's ou 1's à frente dos valores originais).

\begin{codigoMargem}
-- Verificando a extensao de sinal
LTLSPEC G ( num_ext[15:12] = 0b4_0000 | 
            num_ext[15:12] = 0b4_1111 )
LTLSPEC G ( num = 0b12_110100100011 -> 
            num_ext[15:12] = 0b4_1111 )
LTLSPEC G ( num = 0b12_010100100011 -> 
            num_ext[15:12] = 0b4_0000 )
\end{codigoMargem}

\section{Conclusões}

A verificação de propriedades do processador simplificado implementado neste trabalho possibilitou visualizar na prática o que é uma das principais aplicações de \textit{model checking}, que é a verificação de propriedades de circuitos como os de um processador.

Apesar de se tratar de um processador simplificado, foi possível ainda verificar propriedades básicas dos circuitos que envolvem os módulos implementados, de forma a cumprir o objetivo principal do trabalho.

Foram encontradas dificuldades nos testes principalmente em relação ao tempo de execução, o que resultou nas simplificações na implementação do processador anteriormente discutidas. Tentativas de alterar o tamanho da palavra do processador ou o tamanho em bits dos dados armazenados em registradores, entre outras coisas, foram inviabilizadas pelo grande aumento no tempo de execução. Esse aumento no tempo de execução é devido ao problema de explosão de estados estudado, que pode ainda ter sido agravado pelo uso do tipo de dados \texttt{word}, cujas configurações dos bits pode também precisar de verificações.

\newpage
\appendix

\lstset{language=bash,
basicstyle=\footnotesize,       % the size of the fonts that are used for the code
numbers=left,                   % where to put the line-numbers
numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
%showspaces=false,               % show spaces adding particular underscores
showstringspaces=false,         % underline spaces within strings
%showtabs=false,                 % show tabs within strings adding particular underscores
frame=single,	                % adds a frame around the code
tabsize=2,	                % sets default tabsize to 2 spaces
%captionpos=b,                   % sets the caption-position to bottom
%breaklines=true,                % sets automatic line breaking
%breakatwhitespace=false,        % sets if automatic breaks should only happen at whitespace
%title=\lstname,                 % show the filename of files included with \lstinputlisting; also try caption instead of title
%escapeinside={\%*}{*)}          % if you want to add a comment within your code
extendedchars=true,
inputencoding=utf8
}

\section{Listagem do código}

\lstinputlisting[caption=Implementação do Processador]{../src/processor.smv}

\nocite{*}
\bibliographystyle{plain}
%\bibliographystyle{apalike}
\renewcommand{\refname}{Referências}
\addcontentsline{toc}{section}{Referências}
\bibliography{referencias}

\end{document}
